COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002
C00007 ENDMK
C⊗;


(DE TAUT (WFF) (TAUT1 (SIMP WFF)))

(DE TAUT1 (W)  
 (COND
  ((ISCONST W) W)
  (T (TAUT 
       ((LAMBDA (X) (MKAND (SUBST T X W) 
			   (SUBST NIL X W))) 
        (FIRSTVAR W)) ))))


(DE SIMP (W) 
  (COND ((OR (ISCONST W) (ISVAR W)) W)
        ((ISNOT W) (SIMPNOT (SIMP (body W))))
        ((ISOR W)  (SIMPOR (SIMP (lhs W))
			   (SIMP(rhs W))))
        ((ISAND W) (SIMPAND (SIMP (lhs W))
			    (SIMP(rhs W))))
        ((ISIMPLIES W) (SIMPIMP (SIMP (lhs W))
				(SIMP(rhs W))))
        ((ISEQUIV W) (SIMPEQUIV (SIMP (lhs W))
				(SIMP(rhs W)))) ))


(DE SIMPNOT (W) (COND ((ISFALSE W) T) 
		      ((ISTRUE W) NIL) 
		      (T (MKNOT W))))

(DE SIMPOR  (W1 W2) (SIMPANDOR @OR W1 W2 W1 W2))

(DE SIMPAND (W1 W2) (SIMPANDOR @AND W1 W2 W2 W1))

(DE SIMPIMP (W1 W2) (SIMPOR (SIMPNOT W1) W2))

(DE SIMPEQUIV (W1 W2)
    (SIMPAND (SIMPIMP W1 W2)(SIMPIMP W2 W1)))

(DE SIMPANDOR (OP W1 W2 V1 V2)
  (COND	((ISTRUE W1) V1) 
	((ISTRUE W2) V2)
	((ISFALSE W1) V2)
	((ISFALSE W2) V1)
	(T (MKOP OP W1 W2))))


(DE FIRSTVAR (W1)
 (COND ((ISVAR W1) W1)
       ((UNARY W1) (FIRSTVAR (body W1)))
       ((FIRSTVAR (lhs W1)))
       (T (FIRSTVAR (rhs W1)))) )

(DE PN (WFF Z)
 (COND ((ATOM WFF) (COND ((ISEQOR Z) (MKNOT WFF)) (T WFF)))
       ((ISNOT WFF) (PN (body WFF) (FLIP Z)))
       ((ISEQUIV WFF)
         (MKOP Z
	   (MKOP (FLIP Z) 
		 (PN (lhs WFF) (QUOTE OR)) 
		 (PN (rhs WFF) (QUOTE AND)))
           (MKOP (FLIP Z) 
		 (PN (lhs WFF) (QUOTE AND)) 
		 (PN (rhs WFF) (QUOTE OR)))))
        ((ISIMPLIES WFF) (MKOP (FLIP Z) 
			       (PN (lhs WFF) (FLIP Z)) 
			       (PN (rhs WFF) Z)))
        ((ISAND WFF) (MKOP Z 
			   (PN (lhs WFF) Z) 
			   (PN (rhs WFF) Z)))
        ((ISOR WFF) (MKOP (FLIP Z) 
			  (PN (lhs WFF) Z) 
			  (PN (rhs WFF) Z))) ))

(DE ISTRUE    (X) (EQ X T))

(DE ISFALSE   (X) (EQ X NIL))

(DE ISNOT     (X) (EQ (CAR X) (QUOTE NOT)))

(DE ISOR      (X) (EQ (CAR X) (QUOTE OR)))

(DE ISAND     (X) (EQ (CAR X) (QUOTE AND)))

(DE ISIMPLIES (X) (EQ (CAR X) (QUOTE IMPLIES)))

(DE ISEQUIV   (X) (EQ (CAR X) (QUOTE EQUIV)))

(DE ISEQOR    (X) (EQ X (QUOTE OR)))

(DE FLIP (Z) (COND ((EQ Z (QUOTE OR)) (QUOTE AND)) (T (QUOTE OR))) )

(DE lhs (WFF) (CADR WFF))

(DE rhs (WFF) (CADDR WFF))

(DE body (WFF) (CADR WFF))

(DE MKOP (OP X Y) (LIST OP X Y))

(DE MKAND (X Y) (MKOP (QUOTE AND) X Y)) 

(DE MKNOT (X) (LIST (QUOTE NOT) X)) 

(DE ISCONST (W) (OR (EQ W T) (EQ W NIL)))

(DE ISVAR (W) (AND (ATOM W) (NOT (NUMBERP W))))

(DE UNARY (W) (EQ (CAR W) (QUOTE NOT)))

(DE BINARY (W)
  (OR (OR (OR (EQ (CAR W) (QUOTE AND)) 
	      (EQ (CAR W) (QUOTE OR))) 
	  (EQ (CAR W) (QUOTE IMPLIES)))
      (EQ (CAR W) (QUOTE EQUIV))))